# Logic class for the MVL_Toolkit by Koen Lefever 2009-2010, GPL v.3 licensed

import time 

nr_of_propositions = 2              # always create truth tables with 2 input propositions P & Q, even for unary operators
meta_value = "'This is not a truth value.'"                         # sentinel value when searching in truth value aliases

class Logic():
    """Multi-valued Logic class"""
    def __init__(self, truth_values_list, designated_values_list):
        self.nr_of_truth_values = len(truth_values_list)
        if self.nr_of_truth_values < 2:
            raise ValueError('MVL_Toolkit only supports MANY-Valued Logics, please use at least 2 truth values.')
        if meta_value in truth_values_list:
            raise ValueError('You truly defy all logic.')
        for v in truth_values_list:
            if truth_values_list.count(v) > 1:
                raise ValueError('Truth values must be unique')
        self.truth_values_list = truth_values_list
        if len(designated_values_list) < 1:
            raise ValueError('Please assign at least one truth value as being designated.')
        if len(designated_values_list) >= self.nr_of_truth_values:
            raise ValueError('Please assign at least one truth value as being non-designated.')
        for v in designated_values_list:
            if not v in self.truth_values_list:
                raise ValueError('Designated truth value '+str(v)+' not defined as a truth value.')
        self.designated_list = designated_values_list
        self.nr_of_rows = self.nr_of_truth_values ** nr_of_propositions
        self.nr_of_columns = self.nr_of_truth_values ** self.nr_of_rows
        # create 2 columns with all combinations of input propositions
        self.p_column = []
        self.q_column = []
        for t in range(0, self.nr_of_rows):
            num, res = divmod(t, self.nr_of_truth_values)            
            self.p_column.append(self.truth_values_list[num])
            self.q_column.append(self.truth_values_list[res])
        # create list with aliases of truth values
        self.aliases = {}
        for t in self.truth_values_list:
            self.aliases[t] = []

    # conversion methods between representations - base conversions between number systems
    def nr_to_truth_value(self, nr):
        """method to convert an integer to a truth value"""
        nr = int(nr)
        if nr < 0:
            raise ValueError('Truth value number cannot be less than zero')
        if nr > self.nr_of_truth_values:
            raise ValueError('Truth value number cannot be higher than the number of truth values')
        return(self.truth_values_list[nr])
            
    def truth_value_to_nr(self, truth_value, use_aliases = True):
        """method to convert a truth value to an integer"""
        if truth_value in self.truth_values_list:
            return (self.truth_values_list.index(truth_value))
        elif use_aliases:
            search_result = meta_value
            for search in self.truth_values_list:
                if truth_value in self.aliases[search]:
                    search_result = search
                    break
            if not search_result == meta_value:
                return(self.truth_values_list.index(search_result))
        raise ValueError('Undefined truth value: ' + str(truth_value))
        
    def column_to_nr(self, column, use_aliases = True):
        """method to convert a list of truth values to an integer"""
        nr = 0
        power = 0
        column.reverse()
        for v in column:
            nr = nr + self.truth_value_to_nr(v, use_aliases) * (self.nr_of_truth_values ** power)
            power += 1
        return(nr)

    def nr_to_column(self, nr, length = False):
        """method to convert an integer to a list of truth values"""
        nr = int(nr)
        if nr < 0:
            raise ValueError('Column number cannot be less than zero')
        if nr > self.nr_of_columns:
            raise ValueError('Column number cannot be higher than the number of columns')
        if not length:
            length = self.nr_of_rows
        column = []
        while self.nr_of_truth_values <= nr:
            nr, rem = divmod(nr, self.nr_of_truth_values)
            column.insert(0, self.truth_values_list[rem])
        if nr > 0:
            column.insert(0, self.truth_values_list[nr])
        while len(column) < length:
            column.insert(0, self.truth_values_list[0])
        return column
        
    # logical operator function
    def operator(self, nr, p, q, use_aliases = True):
        """operator function for a Logic"""
        column = self.nr_to_column(nr, self.nr_of_rows)
        row = (self.truth_value_to_nr(p, use_aliases) * self.nr_of_truth_values) + self.truth_value_to_nr(q, use_aliases)               
        return(column[row])

    # add aliases for truth values
    # It is not possible to add both 0 and False or both 1 and True by this method, because to Python True == 1 & False == 0
    # This is only an esthetical glitch, since Python will treat them correctly (since they are the same to Python)
    # Write directly to logic_name.aliases[] if you want to have 0, False, 1 and True in the aliases list
    def add_aliases(self, truth_value, aliases_list):
        """add aliases for a truth value"""
        if meta_value in aliases_list:
            raise ValueError('You truly defy all logic.')
        new_list = self.aliases[truth_value]
        for alias in aliases_list:
            if not alias in new_list:
                new_list.append(alias)
        self.aliases[truth_value] = new_list
                
    # function on interpretation level
    def designated(self, truth_value, use_aliases = True):
        """method to check if a truth value is designated"""
        if truth_value in self.designated_list:
            return(True)
        elif use_aliases:            
            for v in self.designated_list:
                if truth_value in self.aliases[v]:
                    return(True)
        return(False)

    # check if an operator is a sheffer function
    # brute force approach, slow, inefficient, keeps complete set in memory
    # not useable, but it's a start.
    # strange bug: every other call, p & q are replaced by NOT p & NOT q
    def sheffer(self, op, verbose = False):
        p = self.column_to_nr(self.p_column, False)
        q = self.column_to_nr(self.q_column, False)
        if verbose:
            print 'examining operator ',op
            print 'start creating list of columns'
        found = []
        for t in range(0, self.nr_of_columns):
            found.append(False)
        if verbose:
            print 'list of columns created'
        generation = 0
        complete = False
        stroke = False
        lastgen = [p, q]
        found[p] = True
        found[q] = True
        nr_found = 2
        if verbose:
            print lastgen
            print 'generation ',generation,' completed, starting with', len(lastgen),' columns. ', time.strftime("%a, %d %b %Y %H:%M:%S", time.localtime())
        while not complete:
            generation += 1
            current = []
            lastgen_indexed = []
            for p in range(0, self.nr_of_columns):
                if p in lastgen:
                    lastgen_indexed.append(True)
                else:
                    lastgen_indexed.append(False)
            for prop1 in lastgen:
                prop1c = self.nr_to_column(prop1)
                for prop2 in range(0, prop1+1):
                    if found[prop2] and not(prop1 < prop2 and lastgen_indexed[prop2]):
                        prop2c = self.nr_to_column(prop2)
                        prop3c = []
                        prop4c = []
                        for t in range(0, self.nr_of_rows):
                            prop3c.append(self.operator(op, prop1c[t], prop2c[t], False))
                            prop4c.append(self.operator(op, prop2c[t], prop1c[t], False))
                        prop3 = self.column_to_nr(prop3c)
                        prop4 = self.column_to_nr(prop4c)
                        if not(found[prop3] or prop3 in current):
                            current.append(prop3)
                            nr_found += 1
                            if nr_found == self.nr_of_columns:
                                stroke = True
                                complete = True
                                if verbose:
                                    print 'Eureka!', time.strftime("%a, %d %b %Y %H:%M:%S", time.localtime())
                        if not(found[prop4] or prop4 in current):
                            current.append(prop4)
                            nr_found += 1
                            if nr_found == self.nr_of_columns:
                                stroke = True
                                complete = True
                                if verbose:
                                    print 'Eureka!', time.strftime("%a, %d %b %Y %H:%M:%S", time.localtime())
                        if complete:
                            if verbose:
                                print 'breaking'
                            break
                if complete:
                    if verbose:
                        print 'breaking'
                    break
            for t in current:
                found[t] = True
            lastgen = current
            if len(current) == 0:
                complete = True
            if verbose:
                #print lastgen
                print 'generation ', generation, ' completed, ', len(lastgen), ' columns generated. ', time.strftime("%a, %d %b %Y %H:%M:%S", time.localtime())
        if verbose:
            if stroke:
                print '========================================================'
            else:
                print '--------------------------------------------------------' 

        return(stroke)
